$\forall$$T$:Type, $l_{1}$,$l_{2}$,$l_{3}$:($T$ List). \\[0ex]iseg($T$; $l_{1}$; append($l_{2}$; $l_{3}$)) \\[0ex]$\Leftarrow\!\Rightarrow$ (iseg($T$; $l_{1}$; $l_{2}$) $\vee$ ($\exists$$l$:$T$ List. ((0 $<$ $\parallel$$l$$\parallel$) $\wedge$ ($l_{1}$ = append($l_{2}$; $l$)) $\wedge$ iseg($T$; $l$; $l_{3}$))))